|
Welcome to the support page for the text Logic, Proof and Computation 3rd edition; henceforth LPC.
What is in the Book?
|
Beginning with a review of formal languages and their syntax and semantics, LPC
conducts a computer assisted course in formal reasoning and the relevance of logic to mathematical proof,
information processing and philosophy.
Topics covered include formal grammars, semantics of formal languages, sequent systems, truth-tables,
propositional and first order logic, identity, proof heuristics, regimentation, set theory, Tarski’s semantic
theory of truth, databases, modal logic, possible world semantics, Herbrand’s proof, automated deduction,
proof by induction, model theory and Skolem’s paradox, Turing machines, undecidability and a computer illustration
of the reasoning underpinning Gödel’s incompleteness proof.
Logic proofs for the student are supported by computer-assisted proofs and the programs are freely
available from this page. LPC is designed as a multidisciplinary reader for students in computing, philosophy
and mathematics.
| 
|
How to Get the Book?
Copies of LPC are available from the
Great British Bookshop. The distribution
extends to the UK, the EC countries and the USA. You may be pleasantly surprised to find the GBB can reach
you if you are outside those countries; so do enquire if so.
Running the Programs for Logic, Proof and Computation
You can download the programs from
here. You need a working Shen image to run the programs.
Errata
LPC was publically available on the 26th May, 2023 and went through a number of changes becoming
'stable' on the 6th June. Here follows a list of errata.
|
Page | Error |
|
57 | The proof, which is inherited from the second edition, is valid, but in the new support software the
ordering of assumptions has changed. In the second edition, the support program was slightly different.
Call this change zero. |
|
58, 61 | Ditto change zero. |
|
141 | The text (R Philip Tully Catiline) should be (R Philip Cicero Catiline) and vice versa. |
|
141 | In a prepublication preprint. You will not find this error in your text. 'if rendered in first-order logic ...
Bush' should be cut. A paste error. |
|
228-231 | The type 'valid' is replaced by 'step'. This is a naming convention. |
|
266 | 'then under v' bottom of page, v should be italicised. |
|
293 | Second example of unification x -> a should be x -> (g y). |
|
302 | Installation routine; this changed somewhat prior to general release. |
Feedback
Do post if you have an issue and
errors will be corrected and you will be placed in the acknowledgements.
|
LATEST NEWS
The open science initiative.
Hundreds of free online pages on Shen technology to appear in 2025.
|
